(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/lists/list.ma".
include "basics/logic.ma".
include "bv/bv-lib.ma".

inductive integer : Type[0] ≝
  int : bool → nat → integer.
  
  
notation "+x" with precedence 80 for @{int true $x}.
notation "-x" with precedence 80 for @{int false $x}.

inductive struct_one : Type[0] ≝
  atom : integer→ struct_one
| unit : struct_one.

inductive operator : Type[0] ≝
  par : operator
| copar : operator
| seq : operator.  

inductive struct : Type[0] ≝
   base : struct_one → struct
|  lista : operator → list struct → struct.

definition eqb_op ≝ λo1,o2.match o1 with[
  par ⇒ match o2 with [ par ⇒ true | _ ⇒ false]
| copar ⇒ match o2 with [copar ⇒ true | _ ⇒ false ]
| seq ⇒ match o2 with [seq ⇒ true | _ ⇒ false]].

(*
lemma eq_op : ∀o1,o2.(eqb_op o1 o2=true) ↔ (o1=o2) .
#O1 #O2 elim O1 elim O2 %
normalize //
#A destruct qed.

lemma eq_op1 : ∀o1,o2.(eqb_op o1 o2=true) → o1=o2.
#O1 #O2 lapply (eq_op O1 O2)
*

 /2/ qed.

lemma eq_op2 : ∀o1,o2.o1=o2→ (eqb_op o1 o2=true).
#O1 #O2 lapply (eq_op O1 O2)
* /2/ qed.
*)



(* Given a list of structures l and an operator op
   create_struct_r replaces every occurrence of 
        lista op sub_l
   in l with
        sub_l                                           *) 
let rec create_struct_r (l:list struct) (op:operator) on l ≝
match l with [
  nil ⇒ [ ]
| cons h tl ⇒ match h with [
          lista sub_op sub_l ⇒ (if (eqb_op sub_op op) then sub_l else h::[])@(create_struct_r tl op)
        | _ ⇒ (h::[])@(create_struct_r tl op)]
].


definition create_struct  ≝λs. match s with [
  base t ⇒ base t 
| lista o l ⇒ lista o (create_struct_r l o)].


(* notation for atoms and unit. For example: «atom n»  with n ∈ ℕ , «unit» *)
(*notation "«x»" with precedence 70 
for @{(*create_struct*) ($x)}.*)

(* usefule abbreviations for atoms*)
notation "𝕒" with precedence 80 for @{base (atom +1)}.
notation "𝕓" with precedence 80 for @{(base (atom +2))}.
notation "𝕔" with precedence 80 for @{(base (atom +3))}.
notation "^𝕒" with precedence 80 for @{(base (atom -1))}.
notation "^𝕓" with precedence 80 for @{(base (atom -2))}.
notation "^𝕔" with precedence 80 for @{(base (atom -3))}.
notation "∘" with precedence 80 for @{(base unit))}.
notation "x+" with precedence 100 for @{(base (atom +($x)))}.
notation "x^" with precedence 100 for @{(base (atom -($x)))}.


(*
notation "𝕒" with precedence 80 for @{(«base (atom +1)»)}.
notation "𝕓" with precedence 80 for @{(«base (atom +2)»)}.
notation "𝕔" with precedence 80 for @{(«base (atom +3)»)}.
notation "^𝕒" with precedence 80 for @{(«base (atom -1)»)}.
notation "^𝕓" with precedence 80 for @{(«base (atom -2)»)}.
notation "^𝕔" with precedence 80 for @{(«base (atom -3)»)}.
notation "∘" with precedence 80 for @{(«unit»))}.
*)


notation "〚 list0 x sep ; 〛"
  non associative with precedence 90
  for @{(*create_struct *)(lista par ${fold right @'nil rec acc @{'cons $x $acc}})}.


notation "❨ list0 x sep ; ❩"
  non associative with precedence 90
  for @{(*create_struct *)(lista copar ${fold right @'nil rec acc @{'cons $x $acc}})}.
  
notation "❮ list0 x sep ; ❯"
  non associative with precedence 90
  for @{(*create_struct*) (lista seq ${fold right @'nil rec acc @{'cons $x $acc}})}.


(*
theorem prova : 
  ∀o.∀l. (All ? (is_ass_norm_1_degree) l) →   is_ass_norm_1_degree (create_struct l o).
#O
elim O
  
  #L
  elim L (*Induco su L*)
    [1,3,5: // (*Se è vuota è banale*) 
    |2,4,6: 
      #H #TL #IND
      (*Forse mi serve parlare di append più che di cons*)
      lapply (append_cons_s ? H  TL) #APPEQ >APPEQ -APPEQ 
      (*Ora spezzo tutte le ipotesi*)
      #HIP lapply (All_append_l ? ? ? ? HIP) * -HIP #HIP1 #HIP2 
      lapply (IND HIP2) -IND #IND 
      lapply HIP1 -HIP1
      elim H (*Induco sulla testa della lista così posso ridurre*)
        [1,3,5:
          #O2 #SUBL #HIP1
          normalize
          lapply HIP1 -HIP1
          (*Ora induco sul secondo operatore:fa esplodere abbastanza la dimostrazione*)
          elim O2 #HIP1           
          normalize
          (*Ora prendo le dimostrazioni con gli operatori uguali*)
          [1,5,9:           
            @All_append_r %
            [2,4,6:
              normalize in IND;
              //
            |1,3,5:
              normalize in HIP1; 
              lapply HIP1 -HIP1 * #HIP1 #T //
            ]
            (*Ora prendo le dimostrazioni con operatori diversi*)
            |2,3,4,6,7,8:  %
            [1,3,5,7,9,11: % #ABS destruct |2,4,6,8,10,12: // ]
          ] |2,4,6: #T #HIP1 @All_append_r % // 
      ]
   ]
qed.
*)


definition neq_op_s ≝λo.λs. match s with [ lista op l ⇒ op≠o | _ ⇒ True].

let rec is_ass_norm s ≝ match s with [
  lista op l ⇒ (All ? (neq_op_s op) l) ∧ (All ? is_ass_norm l)
| base t ⇒ True].

lemma append_cons_s : ∀A.∀a:A.∀l. a::l=[a]@l.
#A #a #L // qed.

lemma All_append_l : ∀A,P,l1,l2.
  All A P (l1 @ l2) → All A P l1 ∧ All A P l2.
  #A #P #L1 #L2 elim L1 normalize 
  [  /2/ ] 
  #H1 #H2 #H3 * #H4 #H5  %
  [ % [ @H4 | lapply (H3 H5) * #H6 #H7 @H6] | lapply (H3 H5) *#H9 #H10 @H10
  ] qed.
  
lemma All_append_r : ∀A,P,l1,l2. All A P l1 ∧ All A P l2 →   All A P (l1 @ l2).
  #A #P #L1 #L2 *
  elim L1 //
  #H #TL
  #IND  #HIP1 #HIP2
  normalize % normalize in HIP1; lapply HIP1 * #H12 #H13 /2/ qed.            
      


definition is_not_unit ≝λs.match s with [base t ⇒ match t with [  unit ⇒ false | _ ⇒ true ] | _ ⇒ true ].
definition filter_unit_base ≝ filter struct is_not_unit.

(* Remove ALL units from struct s, if s is different from unit*)
let rec filter_unit s≝  match s with [
    lista op l ⇒ lista op (filter_unit_base (map ? ? filter_unit l))
  | base t ⇒ base t].
  
  

definition neg_op ≝ λo. match o with [
  par   ⇒ copar
| copar ⇒ par
| seq   ⇒ seq ].


let rec neg s ≝
  match s with [
      lista op l ⇒ lista (neg_op op) (map ? ? neg l) 
    | base t ⇒ match t with [
               atom i ⇒ match i with [ int b n ⇒ base (atom (int (¬b) n)) ]
             | unit  ⇒ base unit  
    ]
  ].
  
let rec size_struct b ≝
  match b with [
     base  t ⇒ 1
  |  lista op l ⇒  (\fold[plus,1]_{i∈l} (size_struct i))].
  
   
   
lemma negbase : ∀t:struct_one.neg (neg (base t) )= (base t).
#T elim T [ #I elim I #B #X elim B normalize // | // qed.
     
     
theorem negIdem : ∀s.neg (neg s) = s.
  #s
  (* Per induzione sulla dimensione dela struttura*) 
  cut (∃n. size_struct s =n)
  
  [% {(size_struct s)} //] (*La dimensione esiste sempre*)
  * #n lapply s -s @(nat_elim1 n) (*Induzione sulla dimensione*)
  -n #m #H #s cases s
  [ #T // (*Caso base*) 
  | (* Se s è una struttura con lista *)
    #O #l 
     cases l (*Induzione sulla lista interna *)
      [ (*Lista vuota*)
        #H1  elim O normalize  //
       | (*Lista con almeno un elemento *)
         #st #l1 #H1 normalize
          @eq_f2 (*Spezzo la lista*)
          [ elim O //] (*Gli operatori non sono rilevanti*)
          @eq_f2
           [ (*Head*)
              @(H … (refl  …)) (*La dimenione della head è minore del totale?*)
              <H1 >(plus_n_O (size_struct st)) in ⊢ (?%?); whd
              >(plus_n_Sm (size_struct st) 0) in ⊢ (?%?); @monotonic_le_plus_r
              elim l1 (*Induzione sulla coda*) // #a #tl normalize /2/ 
           | (*Tail*)
              normalize in H1; lapply(sym_eq nat …H1)  >commutative_plus -H1 #H1 lapply (eq_plus_to_le … H1)-H1 
              elim l1 (*Induzione sulla coda*)
              // (*Coda vuota*)
              #b2 #l2 #Hind normalize #H1 @eq_f2
              [ (*Spezzo la lista, Head*)
                @(H … (refl …)) @(lt_to_le_to_lt … H1) >(plus_n_O (size_struct b2)) in ⊢ (?%?); whd
               >(plus_n_Sm (size_struct b2) 0) in ⊢ (?%?); @monotonic_le_plus_r
               elim l2 // #a #tl normalize /2/
               |
              @Hind /2/
             ] 
        ]
    ] 
 ] qed.
 
  
let rec singleton s ≝ match s with [
  lista o l ⇒ match l with [
      nil ⇒ lista o l (*base unit*)
    | cons h tl ⇒ match tl with [
        nil ⇒ singleton h
      | cons h2 tl2 ⇒ lista o (map ? ? singleton l)]]
| base t ⇒ base t].




(*Theorems on singleton?*)
  
(* Given a  list l = (S1 o1 l1)::...::(Si oi li)::...::(Sn on ln) of structures 
    where if (s1 ox lx) ∈ li → ox≠oi 
    and an operator o
   create_struct yields a structure 
   lista o  (S1' o1' l1')::...::(Si' oi' li')::...::(Sm' om' lm')
   where no one among o1',..., om' can be equal to the given o.    
   

   *)
definition cs ≝λl.λo.lista o (create_struct_r l o).  
theorem create_struct_is_ass_norm: ∀o.∀l.All ? is_ass_norm l → is_ass_norm (cs l o).
(* following the previous theorem *)
  #O elim O #L elim L 
  [1,3,5:  
    normalize * %  //  
  |2,4,6:
    #H #TL #IND lapply (append_cons_s ? H  TL) #APPEQ >APPEQ -APPEQ 
    #HIP lapply (All_append_l ? ? ? ? HIP) * -HIP #HIP1 #HIP2 
    lapply (IND HIP2) -IND #IND lapply HIP1 -HIP1 elim H 
    [1,3,5: 
     #T normalize * #T #T % 
      [1,3,5: % 
        [1,3,5: //
        |2,4,6: lapply IND normalize * //
        ]
      |2,4,6: %
        [1,3,5: //
        |2,4,6: lapply IND normalize * //] ]
      |2,4,6:  
      #O2 #SUBL #HIP1 normalize lapply HIP1 -HIP1 elim O2 #HIP1 normalize
      [1,5,9: 
        % @All_append_r % 
        [1,3,5,7,9,11: 
          lapply HIP1 normalize * -HIP1 * //
        |2,4,6,8,10,12: lapply IND normalize * //
        ]
      |2,3,4,6,7,8:% %  (* Qui le cose si moltiplicano più del dovuto, ma per ora mi accontento di
            saperle chiudere*)
        [1,5,9,13,17,21: % #ABS   destruct
        |2,4,6,8,10,12,14,16,18,20,22,24: lapply IND normalize * //
        |3,7,11,15,19,23: lapply HIP1 normalize * //
        ]
      ]     
    ]
  ]
qed.

notation "x ≡ y" with precedence 45
for @{struct_eq $x $y}.

notation "𝐒" with precedence 45 for @{struct}.


let rec setth (A:Type[0]) (l:list A) (e:A) (n:nat) on n ≝ match n with [
  O ⇒ match l with [
    nil ⇒ [e]
  | cons h tl ⇒ e::tl]
| S x ⇒ match l with [
    nil ⇒ l (*Non si può settare*)
  | cons h tl ⇒ h::(setth A tl e x)]].
  


definition list_swap ≝λA:Type[0].λl:list A.λn1,n2:nat.λd:A. 
  match (leb n1 (|l|) ∧ leb n2 (|l|) ) with [
    true ⇒ (
  let e1 ≝ nth n1 ? l (d(*Non viene mai usato*)) in
  let e2 ≝ nth n2 ? l (d(*Non viene mai  usato*)) in
    setth ? (setth ? l e2 n1) e1 n2)
  | false ⇒ l].  



inductive struct_eq : 𝐒→ 𝐒 → Prop ≝ 
 | eqComm : ∀S1,S2: 𝐒 .              S1 ≡ S2 → S2 ≡ S1
 | eqRif : ∀S1: 𝐒 .                  S1 ≡ S1
 | eqTrans : ∀S1,S2,S3: 𝐒 .          S1 ≡ S2 → S2 ≡ S3 → S1 ≡ S3
 
 | eqUnit : ∀S1,S2:𝐒.               filter_unit S1 ≡ filter_unit S2 → S1 ≡ S2
 
 
 | eqParComm : ∀L1.∀N1,N2.         lista par (L1) ≡ lista par (list_swap ? L1 N1 N2 (base unit))
 | eqCoparComm : ∀L1.∀N1,N2.       lista copar (L1) ≡ lista copar (list_swap ? L1 N1 N2 (base unit))

 | eqSingleton : ∀S1,S2.               singleton S1 ≡ singleton S2 → S1 ≡ S2 
  (*nel singleton come nel filter forse è opportuno averne due, una per ogni lato*)
 
 | eqAss : ∀L1,L2,L3.∀O.           L1@L2=L3 → lista O L3 ≡ lista O ((lista O L1)::L2)    
 | eqAss2 : ∀L1,L2,L3,L4.∀O.             L1@L2@L3=L4 → lista O L4 ≡ lista O (L1@((lista O L2)::L3))
 
 | eqContextUg : ∀S1,S2.            S1=S2 → S1 ≡ S2 (*Forse si può evitare.*)
 
 | eqContext : ∀H1,H2.∀L1,L2.∀O.   H1 ≡ H2 → lista O L1 ≡ lista O L2 → lista O (H1::L1) ≡ lista O (H2::L2).
 
 
 


(*
definition term1 ≝ 〚𝕒;𝕓;❨𝕓;𝕒❩〛.
definition term2 ≝ 〚𝕓;𝕒;❨𝕒;𝕓❩〛.

lemma prova : term1 ≡ term2. normalize 
@eqTrans [ @(lista par (list_swap ? [𝕒;𝕓;❨𝕓;𝕒❩] 0 1 (base unit)))]  // normalize  
 @eqContext1 // @eqContext // @eqSingleton 
normalize @eqTrans [ @(lista copar (list_swap ? [𝕓;𝕒] 0 1 (base unit))) ] //qed. *)

(*
let rec nth_s (s:struct) (g:list nat) (otherw: struct) on g ≝
match s with [
  lista op l ⇒ match g with [
      cons h tl ⇒ nth_s (nth h ? l otherw) tl otherw
    | nil ⇒ s
  ]
| base t ⇒ otherw  (* Or t, who knows?*)
].*)

notation "x ⥤ y" with precedence 45
for @{struct_reduce $x $y}.

inductive struct_reduce : 𝐒 → 𝐒→ Prop ≝ 
  | reduceEq : ∀S1,S2:𝐒.    S1 ≡ S2 → S1 ⥤ S2
  | reduceRif: ∀S.          S ⥤ S
  | reduceTrans:  ∀S1,S2,S3: 𝐒 .          S1 ⥤ S2 → S2 ⥤ S3 → S1 ⥤ S3
  | reduceA :  ∀n:nat.     (base unit) ⥤ 〚n+;n^〛
  | reduceS : ∀R,T,U.      ❨ 〚R;T〛;U❩ ⥤ 〚❨R;U❩;T〛
  | reduceQ : ∀R,T,U,V.     ❮〚R;U〛;〚T;V〛❯ ⥤ 〚❮R;T❯;❮U;V❯〛
  | reduceContext : ∀H1,H2:𝐒.∀L1,L2.∀O. 
                  H1 ⥤ H2 → (lista O L1) ⥤ (lista O L2) → (lista O (H1::L1)) ⥤  (lista O (H2::L2))
                  
  | reduceNeg : ∀S,T. neg S ⥤ neg T → S⥤T (*QUESTA SI PUÒ DERIVARE, MA NON RIESCO*).
  


lemma proviamo :  ∘⥤〚1+; 2+;2^;1^〛.



@(reduceTrans ? (〚1+;1^;2+;2^〛) ?) [ |@reduceEq @eqContext //
@eqTrans [ @(lista par (list_swap ? [2+;2^;1^] 0 1 (base unit))) ] @eqComm // normalize 
@eqTrans [ @(lista par (list_swap ? [1^;2+;2^] 0 2 (base unit))) ] @eqComm //]
@(reduceTrans ? (〚〚𝕒;^𝕒〛;〚𝕓;^𝕓〛〛) ? ) 
[ | @reduceEq  
@eqTrans [ @〚〚1+;1^〛;2+;2^〛  | @eqContext // @eqComm @eqAss //] 
@eqTrans [ @(〚1+;1^;2+;2^〛) | @eqComm 
@(eqAss ([1+;1^]) ? ?) // | // ] ]
@(reduceTrans ? (〚∘;〚2+;2^〛〛) ?) [ 
@(reduceTrans ? (〚∘〛) ? ) [ @reduceEq @eqSingleton normalize // | 

@reduceTrans [ @(〚∘;∘〛) | @reduceEq @eqUnit normalize // |  @reduceContext //
@reduceContext //]] |
@reduceContext // qed.

lemma t1_base : ∀t. ∘ ⥤ 〚base t;neg(base t)〛.
#t 
elim t
[ #I elim I #B #N elim B // normalize 
@reduceTrans
[ @〚N+;N^〛 ] // @reduceEq 
@eqTrans
[ @(lista par (list_swap ? [N+;N^] 0 1 (base unit))) ]
//]
normalize 
@reduceEq @eqComm 
@eqTrans [ @〚∘〛 | @eqUnit normalize // | @eqSingleton normalize //] qed.

lemma for_t1 : ∀o. lista o [ ] ≡ ∘.

#O
@(eqTrans ? (lista O [∘]) ?) [@eqUnit normalize // | @eqSingleton normalize //] qed.

lemma t1_vuoto : ∀O. (∘⥤〚(lista O []); (neg (lista O []))〛).
#O
@reduceEq
        @eqComm 
        @(eqTrans ? 〚(lista O [ ])〛 ?)
      [ @eqContext // elim O normalize @eqSingleton normalize] /2/
      @(eqTrans ? ∘ ? ) //
      @eqComm // qed.

      


lemma par_swap : ∀S1,S2. 〚S1;S2〛≡ 〚S2;S1〛.
#S1 #S2 
@(eqTrans ? (lista par (list_swap ? [S1;S2] 0 1 (base unit))) ?) // qed.

lemma copar_swap : ∀S1,S2. ❨S1;S2❩≡ ❨S2;S1❩.
#S1 #S2 
@(eqTrans ? (lista copar (list_swap ? [S1;S2] 0 1 (base unit))) ?) // qed.
      
      (*

lemma t1_lista : ∀O.∀L.  (∘⥤〚(lista O L); (neg (lista O L))〛).
#O #L 

cases O normalize (*Per casi sugli operatori*)
elim L  [1,3,5: @t1_vuoto]
#H #TL #IND
[
 
(*  Voglio poter applicare questa   ❨ 〚R;T〛;U❩ ⥤ 〚❨R;U❩;T〛*)
(* Porto il copar sulla sinistra*)
@(reduceTrans ? (〚(lista copar (neg H::map ? ? neg TL)); (lista par (H::TL))〛) ? )
  [ | @reduceEq @par_swap]

(*Ora devo creare U grazie l'associatività*)

@(reduceTrans ? (〚(❨neg H;(lista copar (map ? ? neg TL))❩); (lista par (H::TL))〛) ?)
   [ | @reduceEq @eqComm @eqContext [  @eqContext // @eqAss //] //]

(*Ora posso applicare la riduzione sulla parte destra*)

@(reduceTrans ? (❨〚(neg H); (lista par (H::TL))〛; (lista copar (map ? ? neg TL))❩) ?)
   [ | @reduceS]

(*Ora devo accoppiare H e neg H*)

@(reduceTrans ? (❨〚(neg H); H;(lista par (TL))〛; (lista copar (map ? ? neg TL))❩) ?)
  [ | @reduceEq @eqContext // 
  
  @eqContext //
  
    @(eqTrans ? ((lista par (H::TL))) ?)
      [ @eqComm @(eqAss2 [H] ? ? ?) // | @eqSingleton normalize //]]
      
@(reduceTrans ? ❨〚〚(neg H); H〛; (lista par TL)〛; (lista copar (map ? ? neg TL))❩)
  [ | @reduceEq @eqComm 
    @eqContext // @(eqAss2 (nil ?) ([neg H;H]) ) //]
@(reduceTrans ? (❨〚〚(neg H); H〛; (lista par TL)〛; (lista copar (map 𝐒 𝐒 neg TL))❩)
      
      


     
      [ @eqComm @(eqTrans ? (〚(lista par TL);H〛)?) //

      @(eqAss2 (nil ?) ? ? ?) 
        @eqComm
      
      
        @(eqTrans ? (lista par (TL@[H]) ) ?)
            [  | normalize    
    @eqContext //
      @(eqTrans ? (lista par (H::TL)) ?)
        [ @eqComm @eqAss  normalize 
      [
  


*)


lemma for_t1_2 :∀o.lista o [ ] ≡ lista o [∘].
 #O 
 @eqUnit normalize // qed.
 

lemma base_n : ∀n,m. n=m → n+ ≡ m+. // qed.

lemma base_n_ug : ∀n,m. n+=m+ → n=m.
#n #m #hip destruct // qed.

lemma per_base_n : ∀l.∀o. ∃l1.(filter_unit (lista o l))=lista o l1.
#L #O 
normalize
% // qed.
(*

lemma per_base_n2 : ∀l.∀o.∀t.  base t = (filter_unit(lista o l)) → False.
#L #O #T
normalize
#H destruct qed.


lemma base_n : ∀n,m. n+≡m+ → n=m.  
#n #m #h 
cut (n+=m+) 
[ | #h2 destruct //] 
inversion h


*)


     

theorem t1 : ∀s. ∘⥤ 〚s;neg s〛.
#s
  (* Per induzione sulla dimensione dela struttura*) 
  cut (∃n. size_struct s =n)
  
  [% {(size_struct s)} //] (*La dimensione esiste sempre*)
  * #n lapply s -s @(nat_elim1 n) (*Induzione sulla dimensione*)
  -n #m #IND #s cases s
  [ #T #IND @t1_base (*Caso base*) 
  | (* Se s è una struttura con lista *)
    #O #l 
     cases l (*Induzione sulla lista interna *)
      [ #IND (*Lista vuota*)
        @t1_vuoto |
        (*Lista con almeno un elemento *)
         #H #TL #H1 normalize
         cases O normalize (*Per casi sugli operatori*)(*Forse conviene portare i primi due insieme*)
        [1,2:
        [letin head ≝H letin tail ≝ TL letin nHead ≝ (neg H) letin nTail ≝ (map ? ? neg TL)
         | letin head ≝ (neg H) letin tail ≝(map ? ? neg TL) letin nHead ≝ H letin nTail ≝ TL ]
         
        (*  Voglio poter applicare questa   ❨ 〚R;T〛;U❩ ⥤ 〚❨R;U❩;T〛*)
        (* Porto il copar sulla sinistra*)
        [@(reduceTrans ? (〚(lista copar (neg H::map ? ? neg TL)); (lista par (H::TL))〛) ? )
          [ | @reduceEq @par_swap]
        ]

        (*Ora devo creare U grazie l'associatività*)

        @(reduceTrans ? (〚(❨nHead;(lista copar (nTail))❩); (lista par (head::tail))〛) ?)

           [2,4: @reduceEq @eqComm @eqContext [1,3:  @eqContext // @eqAss //] //]

        (*Ora posso applicare la riduzione sulla parte destra*)

        @(reduceTrans ? (❨〚nHead; (lista par (head::tail))〛; (lista copar nTail)❩) ?)
           [2,4: @reduceS]

        (*Ora devo accoppiare H e neg H*)

        @(reduceTrans ? (❨〚(nHead); head;(lista par (tail))〛; (lista copar nTail)❩) ?)
          [2,4: @reduceEq @eqContext // 
          
          @eqContext //
          
            @(eqTrans ? ((lista par (head::tail))) ?)
              [1,3: @eqComm @(eqAss2 [head] ? ? ?) normalize // |2,4: @eqSingleton normalize //]]
              
        @(reduceTrans ? ❨〚〚nHead; head〛; (lista par tail)〛; (lista copar nTail)❩)
          [2,4:  @reduceEq @eqComm 
            @eqContext // @(eqAss2 (nil ?) ([nHead;head]) ) //]
        @(reduceTrans ? (❨〚∘; (lista par tail)〛; (lista copar nTail)❩))
        [2,4: @reduceContext // @reduceContext // 
          @(reduceTrans ?(〚head;nHead〛)?) [2,4: @reduceEq//] 
          [2: @(reduceTrans ? 〚nHead; head〛 ?) [2: @reduceEq @par_swap]]
          normalize
          (*Head*)
              @(IND ? ? ? (refl  …)) (*La dimenione della head è minore del totale?*)
              <H1 >(plus_n_O (size_struct H)) in ⊢ (?%?); whd
              >(plus_n_Sm (size_struct H) 0) in ⊢ (?%?);  @monotonic_le_plus_r
              elim TL (*Induzione sulla coda*) // #H2 #TL2 normalize /2/]             

             (*Tail*)
              normalize in H1; 
              
               lapply(sym_eq nat …H1)  >commutative_plus -H1 #H1 lapply (eq_plus_to_le … H1)-H1
               normalize  
              elim TL
               (*Induzione sulla coda*)
              [1,3: normalize #HIP (*Coda vuota*) 
                @(reduceTrans ? (❨〚∘; 〚〛〛❩) ?) [2,4: @reduceEq 
                  @(eqAss2 ([〚∘; 〚〛〛]) (nil ?) (nil ?) ? copar) //]
                  @reduceEq @eqUnit normalize @eqSingleton normalize @eqComm //
                  
              |2,4: (*Almeno un elemento*)
              #H2 #TL2 #Hind2 normalize #HIP1
              -head -tail -nTail -nHead
              [letin head ≝H2 letin tail ≝ TL2 letin nHead ≝ (neg H2) letin nTail ≝ (map ? ? neg TL2)
              | letin head ≝ (neg H2) letin tail ≝(map ? ? neg TL2) letin nHead ≝ H2 letin nTail ≝ TL2 ]
              (*Tolgo il primo ∘*)
              @(reduceTrans ? (❨〚(lista par (head::tail))〛; (lista copar (nHead::nTail))❩) ?)
              [2,4: @reduceEq @eqUnit normalize //]
              
              @reduceNeg
              normalize
              -head -tail -nTail -nHead
              [letin head ≝H2 letin tail ≝ TL2 letin nHead ≝ (neg H2) letin nTail ≝ (map ? ? neg TL2)
              | letin head ≝ (neg H2) letin tail ≝(map ? ? neg TL2) letin nHead ≝ H2 letin nTail ≝ TL2 ]        
              lapply (negIdem (lista par (head::tail))) #eqL2 normalize in eqL2; >eqL2
              -eqL2 
              normalize
              -head -tail -nTail -nHead
              [letin head ≝H2 letin tail ≝ TL2 letin nHead ≝ (neg H2) letin nTail ≝ (map ? ? neg TL2) 
              | letin head ≝ (neg H2) letin tail ≝(map ? ? neg TL2) letin nHead ≝ H2 letin nTail ≝ TL2 ]
              
              @(reduceTrans ? (〚❨(nHead);lista copar (nTail)❩; (lista par (head::tail))〛) ?)
              [2,4: @reduceEq @eqContext //
              [ |  lapply (negIdem H2) #nH2 >nH2
                  lapply (negIdem (lista copar (H2::TL2))) #nTL2 normalize in nTL2; >nH2 in nTL2; #nTL2 >nTL2]
                [1,2: @(eqTrans ? (lista copar (nHead::nTail)) ?)
                  [2,4:  @eqSingleton  normalize //

                  ] @eqComm  @(eqAss2 [nHead] ? ? ?) normalize   //]]

              
              @(reduceTrans ? (❨〚nHead; (lista par (head::tail))〛;(lista copar nTail)❩) ?)
              [2,4: @reduceS]
              @(reduceTrans ?  (❨〚nHead; head;(lista par tail)〛; (lista copar nTail)❩) ?)
              [2,4: @reduceEq @eqContext // @eqContext // @eqComm
              
              @(eqTrans ? 〚(lista par tail); head〛 ?) // 
              @eqComm
              @(eqTrans ? (lista par (head::tail))?) 
              [2,4:  @eqSingleton normalize //]
              
              @eqComm 
              @(eqTrans ? 〚head;(lista par tail)〛) //
               @(eqAss2 [head] tail ? ?) //]
             @(reduceTrans ?  (❨〚〚nHead; head〛; (lista par tail)〛; (lista copar nTail)❩) ?)
             [2,4: @reduceEq @eqContext // @eqComm @eqAss //]
             @(reduceTrans ?  (❨〚∘; (lista par tail)〛; (lista copar nTail)❩) ?)
             [2,4: @reduceContext // @reduceContext // 
             (*Spezzo la lista, Head*)
             [@(reduceTrans ? 〚head;nHead〛?) [| @reduceEq] [2: @par_swap]]

               
                @(IND … (refl …)) @(lt_to_le_to_lt … HIP1) 
                normalize -head -tail -nHead -nTail
                >(plus_n_O (size_struct H2)) in ⊢ (?%?); whd
               >(plus_n_Sm (size_struct H2) 0) in ⊢ (?%?); 

               @le_plus //
               elim TL2 // #a #tl normalize /2/]
               

               
              @Hind2 /2/
              ]
     |
     
     (*  Voglio poter applicare questa   ❮〚R;U〛;〚T;V〛❯ ⥤ 〚❮R;T❯;❮U;V❯〛*)
        (* Porto il copar sulla sinistra*)

        (*Ora devo creare R grazie l'associatività*)
        letin nHead ≝H letin nTail ≝ TL letin head ≝ (neg H) letin tail ≝ (map ? ? neg TL) 
        @(reduceTrans ? (〚(❮nHead;(lista seq (nTail))❯); (lista seq (head::tail))〛) ?)

           [| @reduceEq @eqComm @eqContext [ @eqContext // @eqAss //] //]

        (*Ora devo creare U*)
        
        @(reduceTrans ? (〚❮nHead; (lista seq nTail)❯; ❮head;(lista seq (tail))❯〛) ?)
         [| @reduceEq @eqComm @eqContext [ @eqContext //] @eqContext // @(eqAss2 ([head]) ? ? ?) normalize //]
        
        (*Ora posso applicare la riduzione sulla parte destra*)
        @(reduceTrans ? (❮〚nHead;head〛;〚(lista seq nTail);(lista seq tail)〛❯) ?)

           [ |@reduceQ]

        @(reduceTrans ? (❮∘; 〚(lista seq nTail); (lista seq tail) 〛❯))
        
        [ | @reduceContext //

          normalize
          (*Head*)
              @(IND ? ? ? (refl  …)) (*La dimenione della head è minore del totale?*)
              <H1 >(plus_n_O (size_struct H)) in ⊢ (?%?); whd
              >(plus_n_Sm (size_struct H) 0) in ⊢ (?%?);  @monotonic_le_plus_r
              elim TL (*Induzione sulla coda*) // #H2 #TL2 normalize /2/]             

             (*Tail*)
              normalize in H1; 
              
               lapply(sym_eq nat …H1)  >commutative_plus -H1 #H1 lapply (eq_plus_to_le … H1)-H1
               normalize  
              elim TL
               (*Induzione sulla coda*)
              [1,3: normalize #HIP (*Coda vuota*) 
              @(reduceTrans ? (❮❮〚〛;〚〛❯❯) ?)
              [ |
              @(reduceTrans ? (❮〚❮❯;❮❯〛❯) ?)
              [| @reduceEq @eqUnit normalize //]
              @reduceContext //

               @(reduceTrans ? 〚❮∘;∘❯;❮∘;∘❯〛?)
               [ | @reduceEq @eqUnit normalize//]
             
               @(reduceTrans ? ❮〚∘;∘〛;〚∘;∘〛❯ ?)
               [ @reduceEq @eqUnit normalize //]
              @reduceQ ] @reduceEq @eqSingleton normalize
              @(eqTrans ? ❮ 〚∘〛;〚∘〛❯?)
              [ | @eqUnit //]
              @eqSingleton normalize @eqUnit normalize @eqComm //

              | (*Almeno un elemento*)
              #H2 #TL2 #Hind2 normalize #HIP1
              -head -tail -nTail -nHead
              letin head ≝H2 letin tail ≝ TL2 letin nHead ≝ (neg H2) letin nTail ≝ (map ? ? neg TL2)              
              (*Tolgo il primo ∘*)
              @(reduceTrans ? (❮〚(lista seq (head::tail)); (lista seq (nHead::nTail))〛❯) ?)
              [ | @reduceEq @eqUnit  normalize //]
              normalize
              
              
              @(reduceTrans ? (❮〚❮(H2);(lista seq TL2)❯; (lista seq (neg H2::map ? ? neg TL2))〛❯) ?)
              [ | @reduceContext // @reduceEq @eqContext // @eqComm  @(eqAss2 [H2] ? ? ? ) //]
              @(reduceTrans ? (❮〚❮(H2);(lista seq TL2)❯; (❮neg H2;lista seq (map ? ? neg TL2)❯)〛❯) ?)
              [ | @reduceContext // @reduceEq @eqContext // @eqContext //@eqComm @(eqAss2 ([neg H2]) ? ? ?) //]
              
              (* ❮〚R;U〛;〚T;V〛❯ ⥤ 〚❮R;T❯;❮U;V❯〛*)
              @(reduceTrans ? (❮❮ 〚(H2);neg H2〛; (〚(lista seq TL2);lista seq (map ? ? neg TL2)〛)❯❯) ?)
              [ |@reduceContext // @(reduceQ H2  (neg H2) (lista seq TL2) (lista seq (map ? ? neg TL2)) )]
              @(reduceTrans ? (❮❮ ∘; (〚(lista seq TL2);lista seq (map ? ? neg TL2)〛)❯❯) ?)
              [| @reduceContext // @reduceContext // 
      
             (*Spezzo la lista, Head*)

               
                @(IND … (refl …)) @(lt_to_le_to_lt … HIP1) 
                normalize
                >(plus_n_O (size_struct H2)) in ⊢ (?%?); whd
               >(plus_n_Sm (size_struct H2) 0) in ⊢ (?%?); 

               @le_plus //
               elim TL2 // #a #tl normalize /2/]
               @(reduceTrans ? (❮∘; 〚(lista seq TL2); (lista seq (map ? ? neg TL2))〛❯)?)
               [ | @reduceEq @eqSingleton normalize //]
               

               
              @Hind2 /2/
              ]

             ] 
             
        ]
    ] qed.
#S
elim S
[ #X elim X [ #I elim I #B #N elim B // normalize 
@reduceTrans
[ @〚N+;N^〛 ] // @reduceEq 
@eqTrans
[ @(lista par (list_swap ? [N+;N^] 0 1 (base unit))) ]
//]
normalize 
@reduceEq @eqComm 
@eqTrans [ @〚∘〛 | @eqUnit normalize // | @eqSingleton normalize //]
|
#O #L
